/* Benchmarks for the PionterC verifier. */

// list insertion

struct list
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @                  (({l}) && list(l->next))
  @ in  list(l)
  @ end
  @*/
struct list* insert(struct list* l, int i, int d)
{
  struct list* p; // points to old list
  struct list* q; // temp pointer
  struct list* s;

  p = l;
  q = l;

  s = alloc (struct list);
  s->data = d;
  s->next = null;

  
  if (p==null)
    return p;
  else 
  {
    q = p->next;
    while (q != null && i>1) /*@ 
                                */
    {
      i = i - 1;
      p = q;
      q = q->next;
    }
    if (i!=1)
      return l;
    else 
    {
      s->next = p->next;
      p->next = s;
      return l;
    }
  }
}


/*@ 
  @*/
